/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package expression;

import core.Node;
import core.UnsatException;
import domain.Domain;

/**
 *
 * @author ddoose
 */
public class Eq extends IntExpr {
    
    public Eq(Node n) {
        super(n);
        current = Domain.BOOLEAN;
        target = Domain.BOOLEAN;
    }
    
    public Eq(Node c, IntExpr[] p) {
        super(c, p);
        current = Domain.BOOLEAN;
        target = Domain.BOOLEAN;
    }

    public boolean same(IntExpr i) {
        return (i instanceof Eq) && sameParameters(i);
    }
    
    public void eval() throws UnsatException {
        Domain a = node.getIntExpr(getParameters().get(0)).current;
        Domain b = node.getIntExpr(getParameters().get(1)).current;
        
        // TRUE
        if (a.isValue() && b.isValue() && (a.getValue() == b.getValue())) {
            reduceCurrent(Domain.TRUE);
        }
        // FALSE
        else if (a.disjoint(b)) {
            reduceCurrent(Domain.FALSE);
        }
    }

    public void propagate() throws UnsatException {
        IntExpr a = node.getIntExpr(getParameters().get(0));
        IntExpr b = node.getIntExpr(getParameters().get(1));
        
        if (target.isTrue()) {
            a.reduceTarget(b.current);
            b.reduceTarget(a.current);
        }
        else if (target.isFalse()) {
            if (a.current.isValue()) {
                b.reduceTarget(a.current.comp());
            }
            if (b.current.isValue()) {
                a.reduceTarget(b.current.comp());
            }
        }
    }
    
    public boolean reduce() {
        return false;
    }
    
    public Eq clone(Node n) {
        Eq eq = new Eq(n);
        eq.clone(this);
        return eq;
    }

    public String toString() {
        return "(" + node.getIntExpr(getParameters().get(0)) + " = " + node.getIntExpr(getParameters().get(1)) +")";
    }
    
    public String pretty() {
        return id + "\t" + current + "\t" + target + "\t" + toString();
    }
}
